;; -*- Mode: Lisp; -*-

;;;; Inequality reasoning module for TGIZMO
;;; Last edited 1/29/93, by KDF

;;; Copyright (c) 1991-1993, Kenneth D. Forbus, Northwestern University,
;;; and Johan de Kleer, the Xerox Corporation.
;;; All rights reserved.

;;; See the file legal.txt for a paragraph stating scope of permission
;;; and disclaimer of warranty.  The above copyright notice and that
;;; paragraph must be included in any separate copy of this file.

(defpackage #:bps/tgizmo/ineqs
  (:use #:cl
        #:bps/tgizmo/defs
        #:bps/tgizmo/mlang
        #:bps/tgizmo/psvs
        #:bps/ltms/all)
  (:export
   #:num-order
   #:individual-of
   #:quantity-of
   #:install-comparison-constraints-if-needed
   #:install-comparison-constraints
   #:update-ineqs-as-needed
   #:greater-than?
   #:less-than?
   #:equal-to?
   #:rel-value
   #:rel-value-clause
   #:comparison?
   #:greater-than!
   #:less-than!
   #:equal-to!
   #:lt-forms
   #:eq-forms
   #:gt-forms
   #:lte-forms
   #:gte-forms
   #:use-transitivity
   #:find-comparison-cycles-for
   #:make-comp-cycle
   #:find-comparison-set
   #:check-comp-cycle
   #:find-cycle-support
   #:signed-form
   #:show-comp-cycles
   #:show-ineqs
   #:a
   #:d))

(in-package #:bps/tgizmo/ineqs)

(proclaim '(special *tgizmo*))

(defun num-order (n1 n2)
  (string< (format nil "~A" n1) (format nil "~A" n2)))

(defun individual-of (q-or-n) ;; Presumes single owner
    (cond ((not (listp q-or-n)) nil)
          ((or (eq (car q-or-n) 'A)
               (eq (car q-or-n) 'D)) (individual-of (cadr q-or-n)))
          (t (cadr q-or-n))))

(defun quantity-of (q-or-n)
  (cond ((null q-or-n) (error "Bad format for quantity: ~A" q-or-n))
        ((not (listp q-or-n)) nil)
        ((or (eq (car q-or-n) 'A) (eq (car q-or-n) 'D)) (cadr q-or-n))
        ((or (null (cdr q-or-n)) (cddr q-or-n))
         (error "Bad format for quantity: ~A" q-or-n))
        (t q-or-n)))

(defun install-comparison-constraints-if-needed (n1 n2 &aux cycles)
  (when (equal n1 n2) (error "Can't do self-comparisons: ~A." n1))
  (if (num-order n2 n1) (psetq n1 n2 n2 n1))
  (unless (member (cons n1 n2) (tgizmo-comparisons *tgizmo*) :TEST #'equal)
    (install-comparison-constraints n1 n2)
    ;; Preprocess connectivity for transitivity inferences
    (setq cycles (find-comparison-cycles-for n1 n2))
    (when cycles
      (debugging-tgizmo :COMP
                        "~%  ..Found new comparison cycles:~%~A" cycles)
      (setf (tgizmo-update-ineqs? *tgizmo*) t)
      (setf (tgizmo-comp-cycles *tgizmo*)
            (nconc cycles
                   (tgizmo-comp-cycles *tgizmo*))))
    ;; Finaly, record the comparison as potentially interesting.
    (push (cons n1 n2) (tgizmo-comparisons *tgizmo*))))

;;;; Internal consistency and updating for comparisons

(defun install-comparison-constraints (n1 n2)
  ;; When one of them is not a quantity, perhaps because
  ;;  the individual in question does not exist,
  ;; the comparison is irrelevant
  (let ((q1 (quantity-of n1))
        (q2 (quantity-of n2))
        (node nil))
    (unless (or q1 q2) (error "Can't compare constants: ~A, ~A" q1 q2))
    (assert! `(:IFF ,(if q1
                         (if q2 `(:OR (:NOT (Quantity ,q1))
                                      (:NOT (Quantity ,q2)))
                           `(:NOT (Quantity ,q1)))
                       `(:NOT (Quantity ,q2)))
                    (:AND (:NOT (,n1 <= ,n2))
                          (:NOT (,n2 <= ,n1))))
             :EXISTENCE-CONSTRAINT)
    ;; Ensure transitivity checked whenever new information
    ;; arrives.
    (setq node (get-tms-node `(,n1 <= ,n2)))
    (push `(update-ineqs-as-needed ,node :TRUE)
          (tms-node-true-rules node))
    (push `(update-ineqs-as-needed ,node :FALSE)
          (tms-node-false-rules node))
    (setq node (get-tms-node `(,n2 <= ,n1)))
    (push `(update-ineqs-as-needed ,node :TRUE)
          (tms-node-true-rules node))
    (push `(update-ineqs-as-needed ,node :FALSE)
          (tms-node-false-rules node))
    node))

(defun update-ineqs-as-needed (node label)
  (setf (tgizmo-update-ineqs? *tgizmo*) t)
  (case label
        (:TRUE (push `(update-ineqs-as-needed ,node ,label)
                     (tms-node-true-rules node)))
        (:FALSE (push `(update-ineqs-as-needed ,node ,label)
                      (tms-node-false-rules node)))
        (t (error "Inappropriate label ~A in update-ineqs-as-needed: ~A."
                  label node))))

;;;; Test predicates

(defun greater-than? (n1 n2)
  (and (true? `(,n2 <= ,n1)) (false? `(,n1 <= ,n2))))

(defun less-than? (n1 n2)
  (and (true? `(,n1 <= ,n2)) (false? `(,n2 <= ,n1))))

(defun equal-to? (n1 n2)
  (and (true? `(,n2 <= ,n1)) (true? `(,n1 <= ,n2))))

(defun rel-value (n1 n2)
  (let ((le `(,n1 <= ,n2))
        (ge `(,n2 <= ,n1)))
    (cond ((true? le)
           (cond ((true? ge) :=)
                 ((false? ge) :<)
                 (t :<=)))
          ((false? le)
           (cond ((true? ge) :>)
                 ((false? ge) :BT)
                 (t :>=)))
          ((true? ge) :>=)
          (t :??))))

(defun rel-value-clause (n1 n2 rel)
  (case rel
        (:<= `(,n1 <= ,n2))
        (:>= `(,n2 <= ,n1))
        (:= `(:AND (,n1 <= ,n2) (,n2 <= ,n1)))
        (:< `(:AND (,n1 <= ,n2) (:NOT (,n2 <= ,n1))))
        (:> `(:AND (:NOT (,n1 <= ,n2)) (,n2 <= ,n1)))))

(defun comparison? (n1 n2 &optional (*tgizmo* *tgizmo*))
  (install-comparison-constraints-if-needed n1 n2)
  (use-transitivity)
  (rel-value n1 n2))

;;;; Helpers for asserting inequalities

(defun greater-than! (n1 n2 &optional (reason :USER))
  (assume! `(:NOT (,n1 <= ,n2)) reason)
  (assume! `(,n2 <= ,n1) reason))

(defun less-than! (n1 n2 &optional (reason :USER))
  (assume! `(,n1 <= ,n2) reason)
  (assume! `(:NOT (,n2 <= ,n1)) reason))

(defun equal-to! (n1 n2 &optional (reason :USER))
  (assume! `(,n1 <= ,n2) reason)
  (assume! `(,n2 <= ,n1) reason))

;;; The next three procedures are used in code which
;;; produces justifications.

(defun lt-forms (n1 n2)
  `((,n1 <= ,n2) (:NOT (,n2 <= ,n1))))

(defun eq-forms (n1 n2)
  `((,n1 <= ,n2) (,n2 <= ,n1)))

(defun gt-forms (n1 n2)
  `((:NOT (,n1 <= ,n2)) (,n2 <= ,n1)))

(defun lte-forms (n1 n2) `((,n1 <= ,n2)))

(defun gte-forms (n1 n2) `((,n2 <= ,n1)))

;;;; Transitivity computations

(defun use-transitivity (&optional (*tgizmo* *tgizmo*))
  (do () ((not (tgizmo-update-ineqs? *tgizmo*)))
      (setf (tgizmo-update-ineqs? *tgizmo*) nil)
      (dolist (cycle (tgizmo-comp-cycles *tgizmo*))
              (check-comp-cycle cycle))
      (tg-run-rules)))

(defun find-comparison-cycles-for (n1 n2)
  ;; Queue entries need to be (<n3> <n1>)
  (do ((queue (mapcar #'(lambda (n) (list n n1))
                      (find-comparison-set n1 n2))
              (nconc (cdr queue) new-entries))
       (new-entries nil nil)
       (cycles nil))
      ((null queue) (mapcar #'make-comp-cycle cycles))
      (cond ((equal (caar queue) n2) ;; Got one
             (push  (car queue) cycles))
            (t (dolist (new-num
                        (find-comparison-set (caar queue)
                                             (cadar queue)))
                       (unless (member new-num
                                       (car queue) :TEST #'equal)
                               (push (cons new-num (car queue))
                                     new-entries)))))))

(defun make-comp-cycle (number-list)
  (do ((nums number-list (cdr nums))
       (cycle nil))
      ((null (cdr nums))
       (nreverse (cons (cons (car nums) (car number-list))
                       cycle)))
      (push (cons (car nums) (cadr nums)) cycle)))

(defun find-comparison-set (n1 &optional (skip nil)
                               &aux others)
  (dolist (other (tg-fetch `(,n1 <= ?other)) others)
          (unless (and skip (equal (third other) skip))
                  (push (third other) others))))


(defun check-comp-cycle (cycle &aux lts gts eqs leqs geqs unks)
  ;; Squeezes out any inferences that can be made via transitivity
  ;; Recall cycle is a list of pairs ((n1 . n2) ... (ni . n1)),
  ;; where comparisons link each of the numbers.
  ;; What to do with a cycle can be defined by analogy with
  ;; BCP on clauses.  That is, some labellings are inconsistent,
  ;; while some partial labellings can lead to others being labelled.
  (dolist (pair cycle)
          (case (rel-value (car pair) (cdr pair))
                (:= (push pair eqs))
                (:< (push pair lts))
                (:> (push pair gts))
                (:<= (push pair leqs))
                (:>= (push pair geqs))
                (:?? (push pair unks))))
  (cond ((cdr unks)) ;; Too many unknowns
        ((null unks) ;; Look for violations, hardening
         (cond ((not (or leqs geqs)) ;; All hard
                (cond ((or (and (null gts) (null lts))
                           (and gts lts))) ;; Okay, all = or mixed
                      (t (contradiction ;; Net > or net <, impossible
                          (find-cycle-support cycle)
                          (tgizmo-ltre *tgizmo*)))))
               ((null leqs) ;; must be geqs
                (cond (lts) ;; Could be either, no constraint
                      (gts ;; Contradiction, net effect must be >
                       (contradiction (find-cycle-support cycle)
                                      (tgizmo-ltre *tgizmo*)))
                      (t ;; geq's -> eq's
                       (assert! `(:IMPLIES
                                  (:AND ,@ (find-cycle-support cycle))
                                  (:AND ,@ (mapcar #'(lambda (pair)
                                                       (rel-value-clause (car pair) (cdr pair)
                                                                         :=))
                                                   geqs)))
                                :HARDENING->=))))
               (t ;; Must be leqs
                (cond (gts) ;; Could be either, no constraint
                      (lts ;; Contradiction, net effect must be <
                       (contradiction (find-cycle-support cycle)
                                      (tgizmo-ltre *tgizmo*)))
                      (t ;; leq's -> eq's
                       (assert! `(:IMPLIES
                                  (:AND ,@ (find-cycle-support cycle))
                                  (:AND ,@ (mapcar #'(lambda (pair)
                                                       (rel-value-clause (car pair) (cdr pair)
                                                                         :=))
                                                   leqs)))
                                :HARDENING-<=))))))
        (t ;; Can last one be concluded?
         (cond ((and lts gts)) ;; no constraint
               (lts (if (null geqs) ;; Last must be gt.
                        (assert! `(:IMPLIES
                                   (:AND ,@ (find-cycle-support cycle))
                                   ,(rel-value-clause (caar unks) (cdar unks) :>))
                                  :>-VIA-TRANS)))
               (gts (if (null leqs) ;; Last must be lt.
                        (assert! `(:IMPLIES
                                   (:AND ,@ (find-cycle-support cycle))
                                   ,(rel-value-clause (caar unks) (cdar unks) :<))
                                 :<-VIA-TRANS)))
               (eqs (assert! `(:IMPLIES ;; Last must be =.
                               (:AND ,@ (find-cycle-support cycle))
                               ,(rel-value-clause (caar unks) (cdar unks) :=))
                             :=-VIA-TRANS))
               ((null geqs) ;; All leq's plus unknown.  Must be geq.
                (assert! `(:IMPLIES (:AND ,@ (find-cycle-support cycle))
                                    ,(rel-value-clause (caar unks) (cdar unks) :>=))
                         :GEQ-VIA-TRANS))
               ((null leqs) ;; All geq's plus unknown.  Must be leq.
                (assert! `(:IMPLIES (:AND ,@ (find-cycle-support cycle))
                                    ,(rel-value-clause (caar unks) (cdar unks) :<=))
                         :LEQ-VIA-TRANS))
               (t (error "Bad length cycle: ~A" cycle))))))

;;; Support code

(defun find-cycle-support (cycle &aux support form)
  (dolist (pair cycle support)
   (when (setq form (signed-form `(,(car pair) <= ,(cdr pair))))
         (push form support))
   (when (setq form (signed-form `(,(cdr pair) <= ,(car pair))))
         (push form support))))

(defun signed-form (form)
  (case (label-of form)
        (:TRUE form)
        (:FALSE (list :NOT form))
        (t nil)))

(defun show-comp-cycles (&optional (*tgizmo* *tgizmo*) &aux (counter 0))
  (dolist (cycle (tgizmo-comp-cycles *tgizmo*))
          (format t "~%~D: " counter)
          (dolist (pair cycle) (format t "~A " (number-string (car pair))))
          (incf counter))
  counter)

(defun show-ineqs (&optional (*tgizmo* *tgizmo*))
  (dolist (comp (tgizmo-comparisons *tgizmo*))
          (format t "~%  ~A ~A ~A" (number-string (car comp))
                  (rel-value (car comp) (cdr comp))
                  (number-string (cdr comp)))))

;;; Test cases

(defvar *ineq-test1*
  '((> (A (T i1)) (A (T i2)))
    (= (A (T i2)) (A (T i3)))
    (> (A (T i3)) (A (T i4)))
    (< (A (T i4)) (A (T i1)))
    (> (A (T i3)) (A (T i1))))) ;; Should be 3 cycles

(defvar *ineq-test2*
  '((> (A (T fred)) (A (T george)))
    (> (A (T george)) (A (T mable)))
    (= (A (T mable)) (A (T anabelle)))
    (> (A (T anabelle)) (A (T pat)))))
